int sum(int lhs, int rhs)
{
    return lhs + rhs;
}

// int callSum()
// {
//     int a = 1, b = 2;
//     int sum_ret;
//     klee_make_symbolic(...);
//     return sum_ret;
//     // return sum(a, b);
// }

int callSum()
{
    int a = 1, b = 2;
    return sum(a, b);
}

int main()
{
    return callSum();
}